A, A':Type.
strong-subtype(A;A')
(B:(A
Type), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'), f, g:a:A fp B(a).
((a:A. B(a) 
C(a)) {f g f g}) | 0,22 |
A, A':Type.
(B:(AType), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'), f, g:a:A fp B(a).
((a:A. B(a) C(a)) {f g f g})
| Definitions | |
| Lemmas |